perm filename REVERS.PPR[W82,JMC] blob
sn#864730 filedate 1982-01-21 generic text, type T, neo UTF8
the proof REVERS:
(DECL (REV1) |GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM |∀U V.REV1(U,V)=IF NULL U THEN V ELSE REV1(CDR U,CAR U~V)|)
2. ∀U V.REV1(U,V)=IF NULL U THEN V ELSE REV1(CDR U,CAR U~V)
deps: NIL
(COMMENTL LNAME DEFINFO)
(∀E PHI |λU.∀V.REV1(U,V)=REVERSE U*V| LISTINDUCTION
|NIL*([1#1#1]($DEFINFO*NIL*$DEFINFO*NIL*$DEFINFO**SIMPINFO*NIL))*NIL*
([1#1#2](&DEFINFO*NIL**SIMPINFO*NIL))*NIL| SORTINFO)
4. (∀X U.(∀V.REV1(U,V)=REVERSE U*V)⊃(∀V.REV1(U,X~V)=REVERSE U*X~V))⊃
(∀U V.REV1(U,V)=REVERSE U*V)
deps: NIL
(ASSUME |∀V.REV1(U,V)=REVERSE U*V|)
5. ∀V.REV1(U,V)=REVERSE U*V
deps: (5)
(TRW |REV1(U,X~V)| |5| SORTINFO)
6. REV1(U,X~V)=REVERSE U*X~V
deps: (5)
(∀I (V) 6)
7. ∀V.REV1(U,X~V)=REVERSE U*X~V
deps: (5)
(CI (5) 7 |NIL|)
8. (∀V.REV1(U,V)=REVERSE U*V)⊃(∀V.REV1(U,X~V)=REVERSE U*X~V)
deps: NIL
(∀I (X U) 8)
9. ∀X U.(∀V.REV1(U,V)=REVERSE U*V)⊃(∀V.REV1(U,X~V)=REVERSE U*X~V)
deps: NIL
(RW 4 |$9*NIL|)
10. ∀U V.REV1(U,V)=REVERSE U*V
deps: NIL